; COMMAND-LINE: --finite-model-find
(set-logic HO_ALL)
(set-info :status sat)
(declare-sort $$unsorted 0)
(declare-fun tptp.mvalid ((-> $$unsorted Bool)) Bool)
(assert (= tptp.mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (@ Phi W)))))
(declare-fun tptp.mforall_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool)
(assert (= tptp.mforall_prop (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) (forall ((P (-> $$unsorted Bool))) (@ (@ Phi P) W)))))
(declare-fun tptp.mnot ((-> $$unsorted Bool) $$unsorted) Bool)
(assert (= tptp.mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (@ Phi W)))))
(declare-fun tptp.mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
(assert (= tptp.mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (@ Phi W) (@ Psi W)))))
(declare-fun tptp.mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
(assert (= tptp.mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (@ (@ (@ tptp.mor (@ tptp.mnot Phi)) Psi) __flatten_var_0))))
(declare-fun tptp.mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
(assert (= tptp.mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (@ (@ R W) V)) (@ Phi V))))))
(assert (not (forall ((R (-> $$unsorted $$unsorted Bool))) (@ tptp.mvalid (@ tptp.mforall_prop (lambda ((A (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (@ (@ tptp.mforall_prop (lambda ((B (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (let ((_let_1 (@ tptp.mbox R))) (@ (@ (@ tptp.mimplies (@ _let_1 (@ (@ tptp.mor A) B))) (@ (@ tptp.mor (@ _let_1 A)) (@ _let_1 B))) __flatten_var_0)))) __flatten_var_0)))))))
(set-info :filename SYO056^1)
(check-sat-assuming ( true ))
